e leaks x to e'
== a:Atom1.
== loc(e) >> a
== & state when e\\x:state@loc(e)\\x>>a
== & e receives a
== & isrcv(e') & sender(e') = e & val(e'):valtype(e')>>a 

latex

---

clarification:

es-leaks(es;e;x;e')
== a:Atom1.
== es-atom(es;es-loc(es; e);a)
== & es-state-when-without(es;e;x):es-state-without(es;es-loc(es; e);x)>>a
== & es-rcv-atom(es;e;a)
== & es-isrcv(es; e')
== & & es-sender(es; e') = e  es-E(es) & es-val(es; e'):es-valtype(es; e')>>a 

latex

Definitions	x:A. B(x), Atom$n, state@i\\x, loc(e), state when e\\x, A, e receives a, A & B, b, isrcv(e), P & Q, s = t, E, sender(e), x:T>>a, valtype(e), val(e)
FDL editor aliases	es-leaks